Transaction-level modeling with SystemC has been very successful indescribing the behavior of embedded systems by providing high-level executablemodels, in which many of them have inherent probabilistic behaviors, e.g.,random data and unreliable components. It thus is crucial to have bothquantitative and qualitative analysis of the probabilities of systemproperties. Such analysis can be conducted by constructing a formal model ofthe system under verification and using Probabilistic Model Checking (PMC).However, this method is infeasible for large systems, due to the state spaceexplosion. In this article, we demonstrate the successful use of StatisticalModel Checking (SMC) to carry out such analysis directly from large SystemCmodels and allow designers to express a wide range of useful properties. Thefirst contribution of this work is a framework to verify properties expressedin Bounded Linear Temporal Logic (BLTL) for SystemC models with both timed andprobabilistic characteristics. Second, the framework allows users to expose arich set of user-code primitives as atomic propositions in BLTL. Moreover,users can define their own fine-grained time resolution rather than theboundary of clock cycles in the SystemC simulation. The third contribution isan implementation of a statistical model checker. It contains an automaticmonitor generation for producing execution traces of themodel-under-verification (MUV), the mechanism for automatically instrumentingthe MUV, and the interaction with statistical model checking algorithms.
展开▼
